perm filename KK[LET,JMC] blob
sn#435527 filedate 1979-04-20 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00011 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 # COMMENT
C00004 00003 # AXIOMS
C00008 00004 # LEMMA 1
C00010 00005 # LEMMA 2
C00011 00006 # LEMMA 3
C00013 00007 # LEMMA 4
C00014 00008 # LEMMA 5
C00016 00009 # LEMMA 6
C00017 00010 # LEMMA 7
C00018 00011 # MAIN THEOREM
C00019 ENDMK
C⊗;
COMMENT # COMMENT
This is an approach to the axiomatization of Mr.S and Mr.P.
Its basic idea is the same of KNOW[E78,JMC].
These are some diffrent symbols:
k for a PAIR of NATNUMs
s(k) for the sum of the two NATNUM in k
p(k) for the product of the two NATNUM in k
We have introduced a few of PREDCONSTs, for abbreviation only.
But there are some important differences between the two
axiomatizations: our axiom SP is weaker, but our axioms LP
and LS are stronger.
The PREDCONSTs R1 R2 and R3 are slightly different,too.
Next follws a complete list of commands of the FOL proof of
R3(k0). The subsequent proof that k0=<4,13> will be purely
arithmetic, and a computer search has been done to confirm
it.
ENDofCOMMENT #
COMMENT # AXIOMS
#
DECLARE INDVAR t ε NATNUM;
DECLARE INDCONST k0 ε OKPAIR;
DECLARE INDVAR k k1 k2 k3 ε OKPAIR;
DECLARE INDCONST RW ε WORLD;
DECLARE INDVAR w w1 w2 w3 ε WORLD;
DECLARE INDCONST S P SP ε PERSON;
DECLARE INDVAR r ε PERSON;
DECLARE OPCONST K(WORLD)=OKPAIR;
DECLARE OPCONST s(OKPAIR)=NATNUM;
DECLARE OPCONST p(OKPAIR)=NATNUM;
DECLARE PREDCONST A(WORLD,WORLD,PERSON,NATNUM);
DECLARE PREDCONST Qs(OKPAIR) Qp(OKPAIR) Q1(OKPAIR) Q2(OKPAIR) Q3(OKPAIR);
DECLARE PREDCONST Bs(WORLD) Bp(WORLD) B1(WORLD) B2(WORLD);
DECLARE PREDCONST R1(OKPAIR) R2(OKPAIR) R3(OKPAIR);
DECLARE PREDCONST C1(WORLD) C2(WORLD);
AXIOM AR: ∀w r t.A(w,w,r,t);;
AXIOM AT: ∀w1 w2 w3 r t.(A(w1,w2,r,t)∧A(w2,w3,r,t)⊃A(w1,w3,r,t));;
AXIOM SP: ∀w1 w2 t.(A(w1,w2,S,t)∨A(w1,w2,P,t)⊃A(w1,w2,SP,t));;
AXIOM RW: k0=K(RW);;
AXIOM OK: ∀w.OK(K(w));;
AXIOM INIT:
∀w w1.(A(RW,w,SP,0)∧A(w,w1,S,0)⊃s(K(w))=s(K(w1))),
∀w w1.(A(RW,w,SP,0)∧A(w,w1,P,0)⊃p(K(w))=p(K(w1))),
∀w k.(A(RW,w,SP,0)∧s(K(w))=s(k)⊃∃w1.(A(w,w1,S,0)∧k=K(w1))),
∀w k.(A(RW,w,SP,0)∧p(K(w))=p(k)⊃∃w1.(A(w,w1,P,0)∧k=K(w1)));;
AXIOM QS: ∀k.(Qs(k)≡∃k1.(s(k)=s(k1)∧¬(k=k1)));;
AXIOM QP: ∀k.(Qp(k)≡∃k1.(p(k)=p(k1)∧¬(k=k1)));;
AXIOM Q:
∀k.(Q1(k)≡∀k1.(s(k)=s(k1)⊃Qp(k1))),
∀k.(Q2(k)≡∀k1.(R1(k1)∧p(k)=p(k1)⊃k=k1)),
∀k.(Q3(k)≡∀k1.(R2(k1)∧s(k)=s(k1)⊃k=k1));;
AXIOM R:
∀k.(R1(k)≡Qs(k)∧Q1(k)),
∀k.(R2(k)≡R1(k)∧Q2(k)),
∀k.(R3(k)≡R2(k)∧Q3(k));;
AXIOM BS: ∀w.(Bs(w)≡∃w1.(A(w,w1,S,0)∧¬(K(w)=K(w1))));;
AXIOM BP: ∀w.(Bp(w)≡∃w1.(A(w,w1,P,0)∧¬(K(w)=K(w1))));;
AXIOM B:
∀w.(B1(w)≡∀w1.(A(w,w1,S,0)⊃Bp(w1))),
∀w.(B2(w)≡∀w1.(A(w,w1,P,1)⊃K(w)=K(w1)));;
AXIOM C:
∀w.(C1(w)≡Bs(w)∧B1(w)),
∀w.(C2(w)≡C1(w)∧B2(w));;
AXIOM SKNPK: B1(RW);;
AXIOM NSK: Bs(RW);;
AXIOM PK: B2(RW);;
AXIOM SK: ∀w.(A(RW,w,S,2)⊃K(RW)=K(w));;
AXIOM LP: ∀w w1.(A(RW,w,SP,0)⊃(A(w,w1,P,1)≡A(w,w1,P,0)∧C1(w1)));;
AXIOM LS: ∀w w1.(A(RW,w,SP,0)⊃(A(w,w1,S,2)≡A(w,w1,S,0)∧C2(w1)));;
COMMENT # LEMMA 1
∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(Qs(k)≡Bs(w)))
#
ASSUME A(RW,w,SP,0)∧k=K(w);
∧E 1 1;
∧E 1,2;
ASSUME Qs(k);
∀E QS k;
TAUT OK(k) 4 5;
TAUT ∃k1.(OK(k1)∧s(k)=s(k1)∧¬(k=k1)) 5 4;
∃E 7 k1;
TAUTEQ A(RW,w,SP,0)∧OK(k1)∧s(k)=s(k1) 2 8;
SUBST 3 IN ↑;
∀E INIT3 w k1;
⊃E 10,11;
∃E 12 w1;
TAUTEQ A(w,w1,S,0)∧¬(K(w)=K(w1)) 3 8 13;
∃I 14 w1;
∀E BS w;
TAUT Bs(w) 16,15;
⊃I 4⊃17;
ASSUME Bs(w);
TAUT ∃w1.(A(w,w1,S,0)∧¬(K(w)=K(w1))) 16 19;
∃E 20 w1;
∀E OK w1;
∀E INIT1 w w1;
TAUTEQ s(K(w))=s(K(w1)) 2 21 22 23;
SUBSTR 3 IN ↑;
∧E 21 2;
SUBSTR 3 IN ↑;
∧I 22∧(25∧27);
∃I 28 K(w1)←k1;
∀E OK w;
SUBSTR 3 IN ↑;
∧I 29 ↑;
TAUT 5:#1 ↑ 5;
⊃I 19⊃↑;
≡I 18 ↑;
⊃I 1⊃↑;
∀I ↑ w k;
COMMENT # LEMMA 2
∀w k.(A(RW,w,SP,0)∧k=K(w)→(Qp(k)≡Bp(w)))
#
ASSUME Qp(k);
∀E QP k;
TAUT OK(k) 38 39;
TAUT ∃k1.(OK(k1)∧(p(k)=p(k1)∧¬(k=k1))) 38 39;
∃E ↑ k1;
TAUTEQ A(RW,w,SP,0)∧OK(k1)∧p(k)=p(k1) 2 42;
SUBST 3 IN ↑;
∀E INIT4 w k1;
⊃E ↑↑,↑;
∃E ↑ w1;
TAUTEQ A(w,w1,P,0)∧¬(K(w)=K(w1)) 3 42 47;
∃I ↑ w1;
∀E BP w;
TAUT Bp(w) 49 50;
⊃I 38⊃↑;
ASSUME Bp(w);
TAUT 50:#2 50 53;
∃E ↑ w1;
∀E INIT2 w w1;
TAUTEQ p(K(w))=p(K(w1)) 2 55 56;
∧E 55 2;
∧I (22 (57 58));
SUBSTR 3 IN ↑;
∃I ↑ K(w1)←k1;
∧I (31 61);
TAUT Qp(k) 39 62;
⊃I 53⊃↑;
≡I 52 ↑;
⊃I 1⊃↑;
∀I ↑ w k;
COMMENT # LEMMA 3
∀w k.(A(RW.w.SP,0)∧k=K(w)→(Q1(k)≡B1(w)))
#
ASSUME Q1(k);
ASSUME A(w,w1,S,0);
TAUT s(K(w))=s(K(w1)) 2 23 69;
SUBSTR 3 IN ↑;
∀E Q1 k;
TAUT ↑:#2 68 ↑;
∧E ↑ 2;
∀E ↑ K(w1);
TAUT Qp(K(w1)) 22 71 75;
∀E SP w w1 0;
∀E AT RW w w1 SP 0;
∀E 67 w1 K(w1);
TAUTEQ Bp(w1) 2 69 76 77 78 79;
⊃I 69⊃↑;
∀I ↑ w1;
∀E B1 w;
TAUT B1(w) 82 83;
⊃I 68⊃↑;
ASSUME B1(w);
ASSUME OK(k1)∧s(k)=s(k1);
∀E INIT3 w k1;
SUBSTR 3 IN ↑;
TAUT ↑:#2 2 87 89;
∃E ↑ w1;
TAUT 83:#2 83 86;
∀E ↑ w1;
TAUTEQ Qp(K(w1)) 2 77 78 79 91 93;
∧E 91 2;
SUBSTR ↑ IN ↑↑;
⊃I 87⊃↑;
∀I ↑ k1;
TAUT Q1(k) 31 72 98;
⊃I 86⊃↑;
≡I 85 100;
⊃I 1⊃↑;
∀I ↑ w k;
COMMENT # LEMMA 4
∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(R1(k)≡C1(w)))
#
∀E R1 k;
∀E C1 w;
TAUT R1(k)≡C1(w) 35 101 104 105;
⊃I 1⊃↑;
∀I ↑ w k;
COMMENT # LEMMA 5
R2(k0)
#
ASSUME C2(RW);
∀E C2 RW;
∀E AR RW SP 0;
∀E 108 RW k0;
TAUT R1(k0) RW 109:112;
TAUT B2(RW) 110 109;
ASSUME R1(k)∧p(k0)=p(k);
TAUT OK(k)∧p(k0)=p(k) ↑ 5 104;
SUBST RW IN ↑;
∀E INIT4 RW k;
TAUT ↑:#2 111 117 118;
∃E ↑ w1;
∀E 108 w1 k;
∀E SP RW w1 0;
TAUT C1(w1) 115 120 121 122;
∀E LP RW w1;
TAUT A(RW,w1,P,1) ↑ 111 123 120;
∀E B2 RW;
MARK M127;
TAUT ↑:#2 ↑ 114;
∀E ↑ w1;
TAUTEQ k0=k RW 120 125 128;
⊃I 115⊃↑;
∀I ↑ k←k1;
∀E Q2 k0;
∀E OK RW;
SUBSTR RW IN ↑;
TAUT 132:#1 132 131 134;
∧I ↑ 113;
∀E R2 k0;
TAUT R2(k0) 136 137;
⊃I 109⊃↑;
∀E C1 RW;
∀E C2 RW;
TAUT R2(k0) 139 140 141 PK NSK SKNPK;
COMMENT # LEMMA 6
∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(R2(k)⊃C2(w)))
#
ASSUME R2(k);
∀E R2 k;
TAUT R1(k) 143 144;
TAUT Q2(k) 143 144;
TAUT C1(w) 145 106;
ASSUME A(w,w1,P,1);
∀E LP w w1;
TAUT C1(w1) 1 148 149;
TAUT A(w,w1,P,0) 1 148 149;
TAUT p(K(w))=p(K(w1)) 56 2 151;
∀E 108 w1 K(w1);
TAUTEQ R1(K(w1)) 1 77 78 150 151 153;
∀E Q2 k;
TAUT 155:#2 146 155;
∧E ↑ 2;
∀E ↑ K(w1);
SUBST 3 IN 158;
TAUTEQ K(w)=K(w1) 154 159 152;
⊃I 148⊃↑;
∀I ↑ w1;
∀E C2 w;
∀E B2 w;
TAUT C2(w) 147 162 163 164;
⊃I 143⊃↑;
⊃I 1⊃↑;
∀I ↑ w k;
COMMENT # LEMMA 7
Q3(k0)
#
ASSUME R2(k1)∧s(k0)=s(k1);
∀E R2 k1;
∀E Q2 k1;
TAUT OK(k1)∧s(k0)=s(k1) 169:171;
∀E INIT3 RW k1;
SUBST RW IN 172;
TAUT ∃w1.(A(RW,w1,S,0)∧k1=K(w1)) 173 174 111;
MARK M176;
∃E ↑ w1;
∀E 168 w1 k1;
∀E LS RW w1;
∀E SK w1;
TAUTEQ k0=k1 RW 111 122 169 176 177 178 179;
⊃I 169⊃↑;
∀I ↑ k1;
∀E Q3 k0;
TAUT Q3(k0) 134 182 183;
COMMENT # MAIN THEOREM
R3(k0)
#
∀E R3 k0;
TAUT R3(k0) ↑ 184 142;